package edu.lambdateacher.reductions;

import edu.lambdateacher.PropertiesManager;
import edu.lambdateacher.awt.MessageDialog;
import edu.lambdateacher.expressions.Abstraction;
import edu.lambdateacher.expressions.Application;
import edu.lambdateacher.expressions.Expression;
import edu.lambdateacher.expressions.Variable;

public class EtaReduction {
	/**
	 * eta_allowed returns true if eta reduction can be performed on this
	 * expression. Note that the reduction must be direct, not on the leftmost
	 * redex. This means that the body of this expression must be an
	 * application. The arg of that application must be a variable with the same
	 * name as the bound variable of this Abstraction. The func of that
	 * application can't contain the bound variable of this abstraction as an
	 * unbound variable.
	 */
	public static boolean etaAllowed(String curboundvar, Expression thebody) {
		if (curboundvar == null) {
			return false;
		}

		if (!(thebody instanceof Application)) {
			return false;
		}

		Application thebodyapp = (Application) thebody;

		// find the argument of the body (skip over any bindings)
		Expression arg = thebodyapp.getArgSkipBindings();

		if (!(arg instanceof Variable)) {
			return false;
		}

		Variable argvar = (Variable) arg;

		if (argvar.getVarName() == null) {
			return false;
		}

		if (!(argvar.getVarName().equals(curboundvar))) {
			return false;
		}

		// we can eta reduce so far
		// now we have to check that this variable name doesn't exist anywhere
		// else unbound
		if (thebodyapp.getFunc() == null) {
			return true;
		}
		if (!(thebodyapp.getFunc().containsUnbound(curboundvar))) {
			return true;
		}

		return false;
	}
	
	public static Expression etaReduce(Abstraction abstraction) {
		String thisstr = abstraction.stringRepresentation(false);
		Expression toreturn = abstraction;
		// check if eta reduction allowed
		boolean eta_allow = abstraction.etaAllowed();
		if (eta_allow == false) {
			// now bring up the explanation dialog
			if (PropertiesManager.expdlogon) {
				String message = "";
				message = message + "The Lambda Abstraction:\n\n" + thisstr + "\n\n";
				message = message + "is not reducable (can't be eta reduced).";

			}
			return toreturn;
		}

		// if we get to here, eta reduction is allowed.
		// first, if the body is a binding, jump the binding part.
		Expression thebody = abstraction.getBodySkipBindings();

		// now set toreturn
		toreturn = ((Application) thebody).getFunc();
		toreturn.setParentModified(true);

		// now bring up the explanation dialog
		if (PropertiesManager.expdlogon) {
			String message = "";
			message = message + "The expression:\n\n" + thisstr + "\n\n";
			message = message + "is being reduced.\n";
			message = message + "This is an ETA reduction, because the abstraction is of ";
			message = message + "the form \\" + abstraction.getBoundVar() + ".(M)(" + abstraction.getBoundVar() + "), ";
			message = message + "where " + abstraction.getBoundVar() + " does not appear free in M\n";
			message = message + "The result of the reduction is:\n";
			message = message + toreturn.stringRepresentation(false);

		}
		// return the result
		return toreturn;

	}
}
